home
***
CD-ROM
|
disk
|
FTP
|
other
***
search
/
Tech Arsenal 1
/
Tech Arsenal (Arsenal Computer).ISO
/
tek-04
/
prolog_2.zip
/
LOGIC.ZIP
/
LOXED.PRO
next >
Wrap
Text File
|
1987-04-03
|
11KB
|
283 lines
/*
Note from Bob: To run this on types FS and higher, you have to
substitute another symbol for "&", or use "hidedef". Also, the
"inttoasc" clause I have included should be replaced by "atoi"
for efficiency. Also note that "members" is a "built-in" in types
FS and higher, so the definition should be deleted.
*/
/* program LOXED.PRO, propositional logic tutorial,
author Xavier Salazar Resines,
27th january 1987 */
?-hidelog; true.
?-op(200,xfy,'<=>').
?-op(190,xfy,'=>').
?-op(180,xfy,'v').
?-op(170,xfy,'&').
?-op(160,fy,'~').
disp_menu :- menu ; true.
menu:- cls,
nl,print(' M E N U'),
nl,nl,print(' i = instructions,'),
nl,nl,print(' o = operators,'),nl,
nl,print(' e = erase argument,'),nl,
nl,print(' a = introduce an argument and test it(end each with `.`),'),
nl,
nl,print(' l = list or test with rules (at end write menu? <RET>),'),
nl,nl,print(' s: exit the program,'),nl,
nl,print(' EXIT the system: s + ^C + s <RET>.'),nl,nl,
print(' Choice (^P) '), ratom(X), X.
i:- ins,ratom(_),menu.
o:- ops,ratom(_),menu.
e:- erase,menu.
a:- prem,ratom(_),menu.
l:- ord.
s.
/* entering premises & conclusion, build list for WANG test */
prem:- cls,print('!! To begin a new process, first: erase'), nl,
print('Erased (y/n)? '), ratom(S),S = 'y',cls,
print('SYSTEM: L O X'),nl,print('Number of premises: '),
rnum(Np),retract(np(Q)),asserta(np(Np)),nl,print('P r e m i s e s :'),
nl,print('-----------------'),nl,expres(Np,T).
prem.
expres(Np,T):- Np =< 0, print('\t','|- '),retract(ergo(X)),read(Erg),
asserta(ergo(Erg)),theorem(T => Erg),!, fail.
expres(Np,T):-
num(N),Q is N+1,Q = 1,!, retract(num(N)), asserta(num(Q)),
makename(Den,[r,Q]), print(Den),print(' '), read(Ter), Z is Np - 1,
asserta(r(Den(Ter))),expres(Z,Ter).
expres(Np,T):-
Np > 0, num(N), Q is N+1,retract(num(N)), asserta(num(Q)),
makename(Den,[r,Q]),print(Den),print(' '),read(Ter),Z is Np - 1,
asserta(r(Den(Ter))),expres(Z,T & Ter).
/* initialize r)ow, j)ustification, ergo (conclusion), num(ber, np (number of
premises, rf (reference number) */
r(nein).
j(nein).
ergo(nein).
num(0).
np(0).
rf(0).
/* print process */
ord:- cls,rf(X), premises(X).
ord:- conclusion.
ord:- np(X),proof(X).
premises(X):- np(R),Z is X + 1, Z =< R, makename(Den,[r,Z]), r(Den(M)),
print(Den(M)),curwh(X,62),print('(P)'),nl,
premises(Z).
conclusion:- ergo(C),np(R), Z is R + 1,print('\t',' |- '),write(C),
curwh(R,60),print('(conclusion) ').
proof(X):- num(Lim), Z is X + 1,Z =< Lim, makename(Den,[r,Z]),r(Den(M)),
makename(Jus,[j,Z]),j(Jus(N)),curwh(Z,1),print(Den(M)),
curwh(Z,62),print(N),nl,proof(Z).
proof(X):- makename(Den,[r,X]),r(Den(M)),Z is X + 1, finis(Z,M).
/* erase an argument */
erase:- retract(r(M)),retract(j(N)),retract(num(P)),asserta(num(0)),
retract(ergo(Q)), asserta(r(nein)),asserta(j(nein)),
asserta(ergo(nein)).
/* modus ponens */
mp(R1, R2) :- r(R1((X => Y))), r(R2(X)),num(Q),Z is Q + 1,
retract(num(Q)),asserta(num(Z)),makename(Den,[r,Z]),asserta(r(Den(Y))),
makename(Jus,[j,Z]),asserta(j(Jus([mp,R1,R2]))),ord.
/* addition */
ad(R1, W):- r(R1(Y)),num(Q),Z is Q + 1,
retract(num(Q)),asserta(num(Z)),makename(Den,[r,Z]),asserta(r(Den((Y v W)))),
makename(Jus,[j,Z]),asserta(j(Jus([ad,R1]))),ord.
/* conjunction */
cj(R1,R2):-r(R1(X)),r(R2(Y)),num(Q),Z is Q + 1,
retract(num(Q)),asserta(num(Z)),makename(Den,[r,Z]),asserta(r(Den((X & Y)))),
makename(Jus,[j,Z]),asserta(j(Jus([cj,R1,R2]))),ord.
/* simplification */
sp(R1):- r(R1((X & Y))), num(Q),Z is Q + 1,retract(num(Q)),asserta(num(Z)),
makename(Den,[r,Z]),asserta(r(Den(X))),makename(Jus,[j,Z]),
asserta(j(Jus([sp,R1]))),ord.
/* commutativity */
cm(R1):- r(R1((X & Y))),num(Q),Z is Q + 1,retract(num(Q)),asserta(num(Z)),
makename(Den,[r,Z]),asserta(r(Den((Y & X)))),makename(Jus,[j,Z]),
asserta(j(Jus([cm,R1]))),ord.
cm(R1):- r(R1((X v Y))),num(Q),Z is Q + 1,retract(num(Q)),asserta(num(Z)),
makename(Den,[r,Z]),asserta(r(Den((Y v X)))),makename(Jus,[j,Z]),
asserta(j(Jus([cm,R1]))),ord.
tr(R1,R2):- r(R1((X => Y))),r(R2((Y => W))),num(Q),Z is Q + 1,retract(num(Q)),
asserta(num(Z)),makename(Den,[r,Z]),asserta(r(Den((X => W)))),makename(Jus,[j,Z]),
asserta(j(Jus([tr,R1,R2]))),ord.
/* de Morgan law */
dm(R1):- r(R1(~(X & Y))),num(Q),Z is Q + 1,retract(num(Q)),asserta(num(Z)),
makename(Den,[r,Z]),asserta(r(Den((~X v ~Y)))),
makename(Jus,[j,Z]),asserta(j(Jus([dm,R1]))),ord.
dm(R1):- r(R1(~(X v Y))),num(Q),Z is Q + 1,retract(num(Q)),asserta(num(Z)),
makename(Den,[r,Z]),asserta(r(Den((~X & ~Y)))),
makename(Jus,[j,Z]),asserta(j(Jus([dm,R1]))),ord.
/* transform => to v, or viceversa, by definition */
df(R1):- r(R1((X => Y))),num(Q),Z is Q + 1,retract(num(Q)),asserta(num(Z)),
makename(Den,[r,Z]),asserta(r(Den((~X v Y)))),makename(Jus,[j,Z]),
asserta(j(Jus([df,R1]))),ord.
df(R1):- r(R1((X v Y))),num(Q),Z is Q + 1,retract(num(Q)),asserta(num(Z)),
makename(Den,[r,Z]),asserta(r(Den((~X => Y)))),makename(Jus,[j,Z]),
asserta(j(Jus([df,R1]))),ord.
/* contraposition */
ct(R1):- r(R1((X => Y))),num(Q),Z is Q + 1,retract(num(Q)),asserta(num(Z)),
makename(Den,[r,Z]),asserta(r(Den((~Y => ~X)))),makename(Jus,[j,Z]),
asserta(j(Jus([ct,R1]))),ord.
/* double negation in a term */
nodn(~ ~ H,H):- !.
nodn(L,L).
/* double negation */
dn(R1):- r(R1((X & Y))),nodn(X,Nx),nodn(Y,Ny),num(Q),Z is Q+1,makename(Den,[r,Z]),
retract(num(Q)),asserta(num(Z)),makename(Jus,[j,Z]),
asserta(j(Jus([dn,R1]))),asserta(r(Den((Nx & Ny)))),ord.
dn(R1) :- r(R1((X => Y))),nodn(X,Nx),nodn(Y,Ny),num(Q),Z is Q+1,
makename(Den,[r,Z]),retract(num(Q)),asserta(num(Z)),makename(Jus,[j,Z]),
asserta(j(Jus([dn,R1]))),asserta(r(Den((Nx => Ny)))),ord.
dn(R1):- r(R1((X v Y))),nodn(X,Nx),nodn(Y,Ny),num(Q),Z is Q+1,makename(Den,[r,Z]),
retract(num(Q)),asserta(num(Z)),makename(Jus,[j,Z]),
asserta(j(Jus([dn,R1]))),asserta(r(Den((Nx v Ny)))),ord.
dn(R1):- r(R1((X <=> Y))),nodn(X,Nx),nodn(Y,Ny),
num(Q),Z is Q+1,makename(Den,[r,Z]),retract(num(Q)),asserta(num(Z)),
makename(Jus,[j,Z]),asserta(j(Jus([dn,R1]))),asserta(r(Den((Nx <=> Ny)))),
ord.
/* double negation in a single term */
dns(R1):- r(R1((X))),nodn(X,Nx),num(Q),Z is Q+1,
makename(Den,[r,Z]),retract(num(Q)),asserta(num(Z)),makename(Jus,[j,Z]),
asserta(j(Jus([dns,R1]))),asserta(r(Den((Nx)))),ord.
/* verification of validity, test by rules */
finis(Z,X):-ergo(Erg),X = Erg,S is Z+1,curwh(S,20),
print(' q.e.d. SYSTEM: L O X'),!.
/* WANG Algorithm */
theorem(T):- prove([] & [] => [] & [T]),!,nl,
print(' VALID argument L O X').
theorem(_):- nl,print('INVALID argument L O X').
prove(E1):- rule(E1,E2),!, prove(E2).
/* v at left. */
prove(L & [H v I|T] => R):- !,
prove(L & [H|T] => R),
prove(L & [I|T] => R).
/* & at right. */
prove(L => R & [H & I|T]):- !,
prove(L => R & [H|T]),
prove(L => R & [I|T]).
/* atom */
prove(L & [H|T] => R):- !,prove([H|L] & T => R).
prove(L => R & [H|T]):- !,prove(L => [H|R] & T).
/* Verify tautology */
prove(T):- tautology(T),!.
prove(_):- fail.
tautology(L & [] => R & []):- members(M,L), members(M,R).
/* => appears in one side */
rule(L & [H => I|T] => R,
L & [~ H v I|T] => R).
rule(L => R & [H => I|T],
L => R & [~ H v I|T]).
/* <=> appears in one side */
rule(L & [H <=> I|T] => R,
L & [(H => I) & (I => H)|T] => R).
rule(L => R & [H <=> I|T], L => R & [(H => I) & (I => H)|T]).
/* appears ~ */
rule(L & [~ H|T] => R & R2, L & T => R & [H|R2]).
rule(L1 & L2 => R & [~ H|T], L1 & [H|L2] => R & T).
/* & at left */
rule(L & [H & I|T] => R, L & [H,I|T] => R).
/* v at right */
rule(L => R & [H v I|T], L => R & [H,I|T]).
/* Ends WANG */
members(H,[H|_]).
members(I,[_|T]):- members(I,T).
ops:- cls,print('SYSTEM: L O X'),nl,
print('operators (ended with a POINT !!!):'),nl,
print('implication: (x => y).'),nl,
print('conjunction: (x & y).'),nl,
print('disyunction: (x v y).'),nl,
print('equivalence: (x <=> y).'),nl,
print('negation: ~x.'),nl,nl,
print('rules:'),nl,
print('mp((p => q),p) => q modus ponens,'),nl,
print('tr((p => q),(q => r)) => (p => r) transitivity,'),nl,
print('dm(~(p & q)) => (~p v ~q) de Morgan,'),nl,
print('dm(~(p v q)) => (~p & ~q) de Morgan,'),nl,
print('df((p => q)) => (~p v q) definition,'),nl,
print('df((p v q)) => (~p => q) definition,'),nl,
print('ct((p => q)) => (~q => ~p) contraposition,'),nl,
print('sp((p & q)) => p simplification,'),nl,
print('cm((p & q)) => (q & p) commutativity,'),nl,
print('cm((p v q)) => (q v p) commutativity,'),nl,
print('ad(p,h) => (p v h) addition (h is external),'),nl,
print('cj(p,q) => (p & q) conjunction,'),nl,
print('dn(R(X,Y)) => double negation expression 2 arguments,'),nl,
print('dns(R) => double negation ONE argument.'),nl,
print('--------------------------------------------------------------------').
ins:- cls,print('SYSTEM: L O X'),nl,print('INSTRUCTIONS'),nl,
print('-------------'),nl,
print('1. ERASE before introducing an argument,'),nl,
print('2. write the premises and after |- write the conclusion,'),nl,
print('3. each premise or conclusion must be ended with a POINT,'),nl,
print('4. after writing the conclusion wait the automatic validity test,'),
nl,print('5. for the TEST use the connectives and operators sintax,'),
nl,print('6. for the TEST write op(r#,r##)? <RET>,'),
nl,print('7. to print the process list: shift + PrtSc,'),nl,
print('8. to print instructions or operators: ^P, at the end ^P'),
nl,print('9. to RETURN TO THE MENU press ` and <RET>.'),nl,
print('NOTES:'),nl,
print('If a double negation occurs in a complex expression, you must'),
nl,print('simplify it first. Example:'),nl,
print(' ((~ ~p => q) & (~ ~q v ~ ~t))'),nl,
print('must be separated in '),nl,
print(' (~ ~p => q) and (~ ~q v ~t) '),
nl,print('Double negations must be separeted between themselves.'),
nl,print('In expressions WITHOUT BINARY connectives,ex: ~ ~p, use dns(R).').
makename( X, [Letter,Number] ) :-
inttoasc( Number, Chars ),
name( Numname, Chars ),
concat( X, [Letter, Numname] ).
inttoasc( N, [C] ) :- N < 10, !, C is N+48.
inttoasc( N, [C|Cs] ) :-
C is (N mod 10) + 48,
N1 is N/10,
inttoasc( N1, Cs ).
?-disp_menu.